It is often desirable to analyze complex systems such as telephone systems, computer networks, and integrated circuits. In the prior art, computer systems have been developed which use state machine models to represent such complex systems and their behaviour. A model is a collection or system of state machines. Computer systems which support the definition and manipulation of such models permit the analysis of the modelled systems. Three examples of the types of analysis that are made possible by such modelling computer systems are verification (including model checking and equivalence checking), test generation, and synthesis. In verification analysis, a computer system permits a model to be created and analyzed to ensure that the modelled system will function correctly. Test generation analysis derives test cases from the model to test the correctness of the system modelled. A computer system may also support functions to permit a model to be defined to represent a system yet to be created. Such models are used, for example, to generate computer software code, or an integrated circuit design. This is a synthesis analysis of the model.
A well-known approach to formally representing a system is for a modelling computer system to use a state machine for model representation. State machine models are used for verification analysis. For example, the SPIN model checker has been used to find errors in the software of a telephone exchange. The computer software code of critical parts of the telephone system was translated to the Promela modelling language. The SPIN model checker analyzed the state machine model as given by the Promela description, and checked for violation of properties that indicates an error in the program (G. J. Holzmann, The model checker SPIN, IEEE Trans on Software Engineering, V 23 N 5 pp 279–295, May 1997; G. J. Holzmann, and M. H. Smith, A practical method for the verification of event driven systems, Proc Int Conf on Software Engineering, ICSE99, Los Angeles pp 597–608, May 1999).
Computer systems that support state machine models may also be used for synthesis. U.S. Pat. No. 5,537,580, Integrated Circuit Fabrication Using State Machine Extraction from Behavioural HDL describes the design of an integrated circuit using a state machine model.
A state machine is defined to have a number of states and transitions (or events). The model represents a system state as a node in the state machine and a system event as a directed edge between nodes. Thus one node at the end of an edge will represent the system state before the event, and the other node will represent the system after the event has occurred.
For complex systems, a model will not have a single large state machine representation but will be defined by a number of components, reflecting the structure of the system. Each component may itself be a model or may be a state machine. Components within such a model have defined interactions. An interaction between two components will cause a state change that is represented in both components.
Computer systems which support analysis carried out on state machine models are subject to the state explosion problem. This occurs when the analysis computes the composition of the model. If there are M components in a model and each component has N states the system, when fully expanded as a result of computing the composition of the system, has N to the exponent M states. For complex systems, computing the fully expanded composition of the system therefore requires significant computing resources.
In the prior art, techniques have been developed to speed up analysis. Many prior art techniques for the analysis of hardware systems use binary decision diagrams (BDDs; J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. H. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proc. of the 5th Annual IEEE Symposium on Logic in Computer Science, pages 428–439, 1990). BDDs represent certain state machines very compactly, and in certain cases efficient analysis of the state machine may be carried out when the model is represented by a BDD.
Other prior art techniques are used to improve the efficiency in the state machine analysis by avoiding redundant computations. For example, the SPIN model checker performs on-the-fly model checking. In this approach the system expands the composition of state machines at the same time it performs the state machine analysis. Thus, if the desired result of the analysis is obtained by expanding only a part of the system, the expansion of the entire system is avoided. Further techniques to avoid redundant computations are partial order reduction and symmetry reduction. (P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems, An Approach to the State-Explosion Problem. LNCS 1032, Springer-Verlag 1996). (Norris Ip and David L. Dill. Better Verification through Symmetry. Formal Methods in System Design, Volume 9, Numbers 1/2, pp 41–75, August 1996)
A third approach is to reduce the size of models prior to analysis. For example, some techniques remove identified redundant elements (U.S. Pat. No. 6,192,505: Method and System for Reducing State Space Variables Prior To Symbolic Model Checking).
The most powerful technique for reducing models is equivalence reduction. This technique replaces the state machine model with the smallest state machine model that has the same properties. Equivalence reductions will yield smaller models than techniques that remove specific redundant elements. Different equivalence relations have been defined, which specify what type of properties must be preserved. For example, observation equivalence is a popular equivalence relation, which allows large amounts of model reduction and has efficient algorithms to compute the reductions (R. Milner. Communication and Concurrency. Prentice-Hall 1989).
However, equivalence reduction alone is often not a practical reduction technique as it depends on expanding the composition. For this reason, other equivalence reduction techniques have been developed. One such prior art technique is compositional minimization. This is a technique that performs equivalence reduction on each component in a compositional state system. After the equivalence reduction has taken place, the system expands the composition of a subset of reduced components, and performs equivalence reduction on the expanded subset, and so on. The system is initially simplified by the expansion of a subset of the reduced components rather on the entire state system. However, compositional minimization is often ineffective since it requires subsets of components to be composed, which results in state explosion. Moreover, it does not use information about interactions of the subset with the rest of the components, so that the expanded state machine model of the subset can be larger than the expanded model of all the components.
Several techniques allow using information about interactions with other components to alleviate the problem of expansion of subsets being larger than the expansion of the whole system. These include the replacement of other components in the model, other than the component of interest, with simple state machines that are defined to have interactions with the component of interest which are supersets of the actual interactions in the model. Another approach is for a system user to provide input to the system to define reductions in the model. However, this approach gives rise to potential errors by the user and is often time consuming and difficult to carry out (S. C. Cheung and J. Kramer. Context Constraints for Compositional Reachability Analysis. ACM Transactions on Software Engineering and Methodology. October 1996; B. Steffen, S. Graf, G. Lüttgen “Compositional Minimization of Finite State Systems”. International Journal on Formal Aspects of Computing, Vol. 8, pp. 607–616, 1996).
Further drawbacks to these techniques are that they require the compositional state system to be expanded, and that the techniques cannot be effectively used in conjunction with techniques that avoid redundant computation.
It is therefore desirable to implement a method and system for reducing compositional state models to a reduced state space where it is possible to avoid having to fully expand the composition of the components in the model.